/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=BDJ20/FONT#10=BDJ20
␈↓ α∧␈↓␈↓ u1


















␈↓ α∧␈↓α␈↓ ∧/THE PROGRAMMING LANGUAGE ELEPHANT

␈↓ α∧␈↓␈↓ ελby John McCarthy

␈↓ α∧␈↓Abstract:␈α∂Elephant␈α∂is␈α∂another␈α∞language␈α∂(like␈α∂Lucid,␈α∂Prolog␈α∞and␈α∂first␈α∂order␈α∂recursive␈α∞programs)
␈↓ α∧␈↓that␈α∂represents␈α∂programs␈α∂as␈α⊂collections␈α∂of␈α∂sentences␈α∂of␈α⊂first␈α∂order␈α∂logic.␈α∂ Elephant␈α⊂differs␈α∂from
␈↓ α∧␈↓previous␈α⊗such␈α↔languages␈α⊗in␈α⊗representing␈α↔variables␈α⊗explicitly␈α⊗as␈α↔functions␈α⊗of␈α⊗time␈α↔and␈α⊗in
␈↓ α∧␈↓considering␈α_the␈α_␈↓↓program␈α_counter␈↓␈α_or␈α_␈↓↓statement␈α_number␈↓␈α_as␈α_just␈α_another␈α→variable.␈α_ Besides
␈↓ α∧␈↓representing␈α⊂ordinary␈α⊂sequential␈α⊂and␈α⊂parallel␈α⊂programs,␈α⊂Elephant␈α⊂can␈α⊂represent␈α⊂programs␈α⊂that
␈↓ α∧␈↓refer␈α
to␈αthe␈α
past␈α
of␈αvariables␈α
and␈αtherefore␈α
avoid␈α
explicit␈αmention␈α
of␈αmany␈α
data␈α
structures.␈α We
␈↓ α∧␈↓argue␈αthat␈αthis␈αfeature␈αis␈α
a␈αnecessary␈αpart␈αof␈αa␈αvery␈α
high␈αlevel␈αlanguage.␈α We␈αalso␈αdiscuss␈α
proving
␈↓ α∧␈↓properties of Elephant programs and notions of equivalence of programs.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u2


␈↓ α∧␈↓1. Introduction

␈↓ α∧␈↓␈↓ αTThe␈α⊂Elephant␈α⊂algorithmic␈α∂language␈α⊂represents␈α⊂program␈α⊂variables␈α∂as␈α⊂functions␈α⊂of␈α⊂a␈α∂time
␈↓ α∧␈↓variable.␈α∩ Thus␈α∪a␈α∩variable␈α∩␈↓↓x␈↓␈α∪of␈α∩an␈α∪Algol␈α∩program␈α∩is␈α∪replaced␈α∩by␈α∩a␈α∪function␈α∩␈↓↓x(t),␈↓␈α∪and␈α∩an
␈↓ α∧␈↓assignment␈αstatement␈α
␈↓↓x := ...␈↓␈αis␈α
replaced␈αby␈αan␈α
equation␈α␈↓↓x(t+1) = ...␈↓␈α
or␈αsometimes␈α␈↓↓x(t) = ...␈↓.␈α
 The
␈↓ α∧␈↓Elephant formalism has two uses.

␈↓ α∧␈↓␈↓ αTFirst,␈α
Elephant␈α
provides␈α
a␈αsimple␈α
way␈α
of␈α
expressing␈αsequential␈α
programs␈α
as␈α
sentences␈α
in␈αa
␈↓ α∧␈↓first␈α
order␈α
theory␈α
which␈α
can␈αthen␈α
be␈α
used␈α
to␈α
prove␈αproperties␈α
of␈α
the␈α
program.␈α
 Elephant␈αdiffers
␈↓ α∧␈↓from␈α⊂the␈α⊃first␈α⊂order␈α⊂representation␈α⊃of␈α⊂recursive␈α⊂programs␈α⊃described␈α⊂in␈α⊂(Cartwright␈α⊃1976)␈α⊂and
␈↓ α∧␈↓(Cartwright␈α∞and␈α∂McCarthy␈α∞1979)␈α∂in␈α∞that␈α∂Elephant␈α∞is␈α∂bottom-up␈α∞instead␈α∂of␈α∞top-down.␈α∂ Once␈α∞a
␈↓ α∧␈↓program␈α∀has␈α∀been␈α∪expressed␈α∀in␈α∀Elephant,␈α∀the␈α∪␈↓↓inductive␈α∀assertion␈↓␈α∀and␈α∀␈↓↓intermittent␈α∪assertion␈↓
␈↓ α∧␈↓methods␈α
are␈αautomatically␈α
available␈αas␈α
particular␈α
techniques␈αof␈α
making␈αproofs␈α
within␈α
first␈αorder
␈↓ α∧␈↓logic.␈α∞ They␈α
amount␈α∞to␈α
using␈α∞particular␈α
kinds␈α∞of␈α
lemmas␈α∞in␈α
proving␈α∞theorems.␈α
 Instances␈α∞of␈α
the
␈↓ α∧␈↓Hoare axioms are probably also just lemmas.

␈↓ α∧␈↓␈↓ αTThe␈α∂second␈α∂aspect␈α∂of␈α∂Elephant␈α∂is␈α∂the␈α∂ability␈α∂to␈α∂refer␈α∂to␈α∂the␈α∂whole␈α∂past␈α∂of␈α⊂the␈α∂variables
␈↓ α∧␈↓without␈αspecifying␈αdata␈αstructures␈α
for␈αremembering␈αwhat␈αhas␈αto␈α
be␈αknown␈αin␈αorder␈αto␈α
perform␈αa
␈↓ α∧␈↓current␈α
action.␈α
 Thus␈α
a␈α
reservation␈αprogram␈α
written␈α
in␈α
Elephant␈α
can␈αsay␈α
that␈α
a␈α
passenger␈α
has␈αa
␈↓ α∧␈↓reservation␈α∂if␈α∂he␈α∂has␈α∂made␈α∂one␈α∂and␈α⊂not␈α∂cancelled␈α∂it␈α∂without␈α∂specifying␈α∂any␈α∂data␈α⊂structure␈α∂for
␈↓ α∧␈↓remembering who has reservations.  Thus an elephant never forgets.

␈↓ α∧␈↓␈↓ αTThis␈α
ability␈α
to␈α
refer␈α
to␈α
the␈α
past␈α
is␈α
certainly␈α
used␈α
in␈α
informal␈α
English␈α
descriptions␈α
of␈α
what␈α
we
␈↓ α∧␈↓want␈αa␈αcomputer␈αto␈αdo.␈α Therefore,␈αa␈αsufficiently␈αhigh␈αlevel␈αprogramming␈αlanguage␈αmust␈αhave␈αit.
␈↓ α∧␈↓On␈α
the␈αother␈α
hand,␈αthe␈α
Elephant␈αprograms␈α
that␈αI␈α
have␈αbeen␈α
able␈αto␈α
write␈αthat␈α
refer␈αto␈α
the␈αpast
␈↓ α∧␈↓are␈αoften␈αmore␈αdifficult␈αto␈αwrite␈αand␈αread␈αthan␈αprograms␈αwith␈αexplicit␈αdata␈αstructures.␈α Perhaps␈αI
␈↓ α∧␈↓am␈α
simply␈α∞inexperienced␈α
in␈α
writing␈α∞Elephant␈α
program,␈α
perhaps␈α∞extensions␈α
to␈α
the␈α∞formalism␈α
are
␈↓ α∧␈↓needed,␈α∞and␈α∂perhaps␈α∞an␈α∞approach␈α∂different␈α∞from␈α∞Elephant␈α∂will␈α∞work␈α∞better␈α∂in␈α∞referring␈α∂to␈α∞the
␈↓ α∧␈↓past.

␈↓ α∧␈↓␈↓ αTThe simplest way to begin is with examples.

␈↓ α∧␈↓2. Translating a sequential program into Elephant

␈↓ α∧␈↓␈↓ αTConsider␈α⊂the␈α⊃following␈α⊂Algol␈α⊃60␈α⊂program␈α⊃fragment␈α⊂(declarations␈α⊃are␈α⊂omitted)␈α⊃for␈α⊂doing
␈↓ α∧␈↓multiplication by addition:

␈↓ α∧␈↓↓␈↓ αTi := n;␈↓ ¬T0
␈↓ α∧␈↓↓␈↓ αTp := 0;␈↓ ¬T1
␈↓ α∧␈↓↓loop:   ␈↓αif␈↓↓ i = 0 ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;␈↓ ¬T2
␈↓ α∧␈↓↓␈↓ αTi := i - 1;␈↓ ¬T3
␈↓ α∧␈↓↓␈↓ αTp := p + m;␈↓ ¬T4
␈↓ α∧␈↓↓␈↓ αT␈↓αgo to␈↓↓ loop;␈↓ ¬T5
␈↓ α∧␈↓↓done:␈↓ ¬T6

␈↓ α∧␈↓The corresponding Elephant program consists of the equations

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN n
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u3


␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE i(t)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 4 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE p(t)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 2 ∧ i(t) = 0 THEN 6
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 5 THEN 2
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTIn␈α∂these␈α∂equations␈α∂␈↓↓i(t)␈↓␈α∂and␈α∂␈↓↓p(t)␈↓␈α∂replace␈α∞the␈α∂simple␈α∂variables␈α∂of␈α∂the␈α∂Algol␈α∂program.␈α∞ The
␈↓ α∧␈↓function␈α⊃␈↓↓pc(t)␈↓␈α⊂is␈α⊃the␈α⊂program␈α⊃counter,␈α⊂and␈α⊃it␈α⊃takes␈α⊂values␈α⊃from␈α⊂1␈α⊃to␈α⊂6,␈α⊃corresponding␈α⊃to␈α⊂the
␈↓ α∧␈↓numbers␈αwritten␈αon␈α
the␈αright␈αof␈α
the␈αAlgol␈αprogram.␈α
 It␈αshould␈αbe␈α
apparent␈αfrom␈αthe␈αexample␈α
that
␈↓ α∧␈↓any␈αprogram␈αmade␈αup␈αof␈αassignments␈α
and␈α␈↓αgo to␈↓s␈αcan␈αbe␈αsystematically␈αtranslated␈αto␈α
an␈αElephant
␈↓ α∧␈↓program.␈α We␈αhave␈α
used␈αthe␈αlogical␈α
conditional␈αexpression␈α␈↓↓IF ... THEN ... ELSE␈↓␈α
rather␈αthan
␈↓ α∧␈↓␈↓αif␈↓ ... ␈↓αthen␈↓ ... ␈↓αelse␈↓,␈αbecause␈αthere␈αis␈αno␈αreason␈αto␈αprovide␈αfor␈αan␈αundefined␈αcase.␈α (The␈αdistinction␈αis
␈↓ α∧␈↓discussed␈α
in␈α
(Cartwright␈αand␈α
McCarthy␈α
1979)).␈α
 If␈αthe␈α
reader␈α
is␈α
a␈αreactionary␈α
and␈α
refuses␈αto␈α
admit
␈↓ α∧␈↓conditional␈α
expressions␈α
as␈α
terms␈α
in␈α
first␈α
order␈α
logic,␈α
then␈α
they␈α
can␈α
be␈α
eliminated.␈α∞ The␈α
equation
␈↓ α∧␈↓for ␈↓↓i(t+1)␈↓ would then split into the three cases

␈↓ α∧␈↓↓∀t.[pc(t) = 0 ⊃ i(t+1) = 0 ∧ pc(t) = 1 ⊃ i(t+1) = i(t) - 1
␈↓ α∧␈↓↓␈↓ β∧∧ pc(t) ≠ 0 ∧ pc(t) ≠ 1 ⊃ i(t+1) = i(t)]

␈↓ α∧␈↓␈↓ αTNotice␈α∞also␈α∞that␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Elephant␈α∞program␈α∂is␈α∞linear␈α∞in␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Algol
␈↓ α∧␈↓program.

␈↓ α∧␈↓␈↓ αTHaving␈αone␈α
value␈αof␈α␈↓↓pc(t)␈↓␈α
for␈αeach␈αstatement␈α
in␈αthe␈αAlgol␈α
program␈αis␈αunnecessary,␈α
although
␈↓ α∧␈↓it␈αmakes␈αthe␈αsystematic␈αcharacter␈αof␈αthe␈αtranslation␈αmore␈αapparent.␈α If␈αwe␈αlet␈α␈↓↓pc(t) = 0␈↓␈αcorrespond
␈↓ α∧␈↓to␈α
the␈αinitialization,␈α
␈↓↓pc(t) = 1␈↓␈αcorrespond␈α
to␈α
the␈αloop,␈α
and␈α␈↓↓pc(t) = 2␈↓␈α
correspond␈αto␈α
the␈α
label␈α␈↓↓done,␈↓
␈↓ α∧␈↓then the equations become

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE i(t)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE p(t)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 ∧ i(t) ≠ 0 THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTThe correctness of the first version of the Elephant program is given by the sentence
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u4


␈↓ α∧␈↓␈↓ αT␈↓↓∀m n ∃t.[pc(t) = 6 ∧ p(t) = mn]␈↓,

␈↓ α∧␈↓while␈α∀the␈α∪modified␈α∀program␈α∪would␈α∀have␈α∀the␈α∪same␈α∀correctness␈α∪condition␈α∀except␈α∀for␈α∪having
␈↓ α∧␈↓␈↓↓pc(t) = 2␈↓␈αinstead␈αof␈α␈↓↓pc(t) = 6.␈↓␈αEither␈αstatement␈αis␈αprovable␈αfrom␈αany␈αfirst␈αorder␈αaxiomatization␈αof
␈↓ α∧␈↓arithmetic␈αtogether␈αwith␈αthe␈αsentences␈αconstituting␈αthe␈αprogram.␈α No␈αspecial␈αaxioms␈αfor␈αprograms
␈↓ α∧␈↓or "logic of programs" is required.

␈↓ α∧␈↓␈↓ αTThus␈α
an␈α
entirely␈α
conventional␈α
mathematical␈α
way␈α
of␈α
writing␈α
recursion␈α
equations␈α
leads␈α∞to␈α
a
␈↓ α∧␈↓convenient␈α∂programming␈α∂language.␈α∞ I␈α∂am␈α∂tempted␈α∂to␈α∞call␈α∂the␈α∂language␈α∞Algol␈α∂50,␈α∂since␈α∂it␈α∞could
␈↓ α∧␈↓easily have been developed at that time.

␈↓ α∧␈↓␈↓ αTThe␈α
proof␈α
of␈α
correctness␈α
for␈α
this␈αmultiplication␈α
program␈α
is␈α
misleadingly␈α
simple,␈α
since␈αwe␈α
can
␈↓ α∧␈↓easily␈αwrite␈αexplicit␈αformulas␈αfor␈α␈↓↓i(t),␈↓␈α␈↓↓p(t),␈↓␈αand␈α␈↓↓pc(t)␈↓␈αand␈αprove␈αthem␈αby␈αmathematical␈αinduction.
␈↓ α∧␈↓More␈α
typical␈α
proofs␈α
occur␈α
when␈α
it␈α
isn't␈α
convenient␈α
to␈α
give␈α
explicit␈α
formulas␈α
for␈α
the␈α
variables␈αas
␈↓ α∧␈↓functions␈α
of␈α
time␈α
or␈α
for␈αthe␈α
value␈α
of␈α
␈↓↓t␈↓␈α
for␈αwhich␈α
the␈α
program␈α
terminates.␈α
 Then␈αthe␈α
computational
␈↓ α∧␈↓content␈α⊃of␈α⊃the␈α⊃proof␈α⊃is␈α⊃is␈α⊃often␈α⊃essentially␈α⊃the␈α⊃same␈α⊃as␈α⊃that␈α⊃of␈α⊃an␈α⊃␈↓↓inductive␈α∩assertions␈↓␈α⊃proof
␈↓ α∧␈↓combined␈α∀with␈α∀induction␈α∀on␈α∀a␈α∀rank␈α∀function␈α∪of␈α∀the␈α∀variables␈α∀taking␈α∀values␈α∀in␈α∀a␈α∪suitable
␈↓ α∧␈↓inductively ordered set.

␈↓ α∧␈↓3. Reversing a list

␈↓ α∧␈↓␈↓ αTReversing␈α
a␈α
list␈α
provides␈α
another␈α
example␈αof␈α
an␈α
Elephant␈α
program␈α
that␈α
can␈α
be␈αcompared
␈↓ α∧␈↓with␈α∂a␈α∂recursive␈α∂conditional␈α∂expression␈α∂program␈α∂for␈α∂the␈α∂same␈α∂function.␈α∂ We␈α∂start␈α∂with␈α⊂a␈α∂Lisp
␈↓ α∧␈↓"program feature" program written in the style of Algol 60.

␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := w;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := ␈↓NIL␈↓↓;
␈↓ α∧␈↓↓␈↓ αT␈↓ α∧loop:␈↓ αt␈↓αif␈↓↓ null u ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := [␈↓αa␈↓↓ u] . v;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := ␈↓αd␈↓↓ u;
␈↓ α∧␈↓↓␈↓ αT␈↓ αt␈↓αgo to␈↓↓ loop;


␈↓ α∧␈↓␈↓ αTThe corresponding Elephant program is

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[u(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN w
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αd␈↓↓ u(t)
␈↓ α∧␈↓↓␈↓ β4ELSE u(t)],

␈↓ α∧␈↓↓∀t.[v(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αa␈↓↓ u(t) . v(t)
␈↓ α∧␈↓↓␈↓ β4ELSE v(t)]

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 ∧ ¬null u(t) THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTThis can be compared with the LISP program ␈↓↓reverse␈↓ defined by
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u5


␈↓ α∧␈↓␈↓ αT␈↓↓reverse u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ reverse ␈↓αd␈↓↓ u * <␈↓αa␈↓↓ u>␈↓.

␈↓ α∧␈↓With␈α∂the␈α∂latter,␈α∂as␈α⊂shown␈α∂in␈α∂(Cartwright␈α∂and␈α∂McCarthy␈α⊂1979),␈α∂it␈α∂is␈α∂convenient␈α∂to␈α⊂prove␈α∂such
␈↓ α∧␈↓properties␈α⊗as␈α∃␈↓↓reverse reverse u = u␈↓␈α⊗and␈α∃␈↓↓reverse[u * v] = reverse v * reverse u␈↓.␈α⊗ The␈α⊗major␈α∃fact
␈↓ α∧␈↓about the Elephant program is expressed by

␈↓ α∧␈↓␈↓ αT␈↓↓∃t.(pc(t) = 2 ∧ v(t) = reverse w)␈↓.

␈↓ α∧␈↓It␈αcan␈αbe␈αproved␈αby␈αproving␈αthat␈α␈↓↓length␈αu(t)␈↓␈αis␈αa␈αdecreasing␈αfunction␈αof␈α␈↓↓t,␈↓␈αi.e.␈αfor␈αany␈α␈↓↓t␈↓␈αsuch␈αthat
␈↓ α∧␈↓␈↓↓pc(t) < 2,␈↓ there is ␈↓↓t' > t␈↓ such that ␈↓↓length u(t') < length t␈↓, and also that

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[reverse w = reverse u(t) * v(t)]␈↓.

␈↓ α∧␈↓This␈α
is␈α
just␈αanother␈α
␈↓↓inductive␈α
assertions␈↓␈α
proof.␈α So␈α
far␈α
it␈α
seems␈αthat␈α
the␈α
most␈αconvenient␈α
technique
␈↓ α∧␈↓for␈αproving␈αfacts␈αabout␈α
Elephant␈αprograms␈αis␈α␈↓↓inductive␈αassertions␈↓,␈α
which␈αis␈αless␈αflexible␈α
than␈αthe
␈↓ α∧␈↓technique␈αdescribed␈αin␈α(Cartwright␈αand␈αMcCarthy␈α1979)␈αthat␈αuses␈αthe␈α␈↓↓functional␈αequation␈↓␈αand␈α
the
␈↓ α∧␈↓␈↓↓minimization␈α
schema␈↓.␈α This␈α
is␈αbecause␈α
␈↓↓inductive␈α
assertions␈↓␈αprovides␈α
no␈αway␈α
of␈αexpressing␈α
algebraic
␈↓ α∧␈↓relations among functions defined by programs.

␈↓ α∧␈↓␈↓ αTOne␈α
mathematically␈α
straightforward␈α
way␈α
of␈α
defining␈α
functions␈α
by␈α
programs␈α
is␈αthe␈α
following.
␈↓ α∧␈↓We␈α
rewrite␈α
the␈α
above␈α
equations␈α
to␈α
introduce␈α
␈↓↓w␈↓␈α
as␈α
an␈α
explicit␈α
argument␈α
of␈α
the␈α
functions␈α
so␈αthat
␈↓ α∧␈↓they become ␈↓↓u(t,w),␈↓ ␈↓↓v(t,w),␈↓ and pc(t,w).  We then define a relation ␈↓↓reverses(v,w)␈↓ by

␈↓ α∧␈↓␈↓ αT␈↓↓∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))␈↓.

␈↓ α∧␈↓When␈α∂we␈α∂have␈α∞proved␈α∂␈↓↓∀w␈α∂∃!v.reverses(v,w)␈↓,␈α∂first␈α∞order␈α∂logic␈α∂entitles␈α∞us␈α∂to␈α∂replace␈α∂the␈α∞relation
␈↓ α∧␈↓␈↓↓reverses␈↓ by a function.  We can then prove successively that this function satisfies the relations

␈↓ α∧␈↓␈↓ αT␈↓↓reverse ␈↓NIL␈↓↓ = ␈↓NIL␈↓↓␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓reverse [x . u] = reverse u * <x>␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓reverse reverse u = u␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓reverse[u * v] = reverse v * reverese u␈↓,

␈↓ α∧␈↓where the notation is as in (McCarthy and Talcott 1979).

␈↓ α∧␈↓4. Non Immediate Elephant Programs

␈↓ α∧␈↓␈↓ αTWhen␈αwe␈αtranslate␈αan␈αAlgol␈αprogram␈αinto␈αElephant,␈αwe␈αget␈αequations␈αin␈αwhich␈α
the␈α␈↓↓x(t+1)␈↓s
␈↓ α∧␈↓depend␈α
only␈α
on␈α
the␈α
␈↓↓x(t)␈↓s.␈α
 We␈α
will␈α
call␈α
such␈α
a␈α
program␈α
an␈α
␈↓↓immediate␈↓␈α
Elephant␈α
program.␈α
 However,
␈↓ α∧␈↓the␈αrecursion␈αequations␈αwill␈αstill␈αhave␈αguaranteed␈αsolutions␈αif␈αthe␈α␈↓↓x(t)␈↓s␈αdepend␈αon␈αarbitrary␈α
earlier
␈↓ α∧␈↓values of ␈↓↓t.␈↓ This leads to a "high level" programming language with the following features:

␈↓ α∧␈↓␈↓ αT1.␈α∞The␈α
program␈α∞refers␈α∞to␈α
the␈α∞past␈α
through␈α∞earlier␈α∞values␈α
of␈α∞␈↓↓t,␈↓␈α
just␈α∞as␈α∞though␈α
everything
␈↓ α∧␈↓were remembered.  That's why we call the language Elephant, since an Elephant never forgets.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u6


␈↓ α∧␈↓␈↓ αT2.␈α
The␈αcompiler␈α
is␈α
smart␈αand␈α
decides␈αwhat␈α
data␈α
structures␈αare␈α
required␈α
in␈αorder␈α
to␈αcarry␈α
out
␈↓ α∧␈↓the␈α
computations␈α
without␈α
remembering␈α
everything.␈α∞ To␈α
the␈α
extent␈α
that␈α
compilers␈α
can␈α∞be␈α
written
␈↓ α∧␈↓that␈α
do␈α
this␈α
effectively,␈αElephant␈α
is␈α
a␈α
"higher␈α
level"␈αlanguage␈α
in␈α
which␈α
the␈α
programer␈αspecifies␈α
less
␈↓ α∧␈↓than in Algol, etc.

␈↓ α∧␈↓5. An airline reservation system

␈↓ α∧␈↓␈↓ αTConsider␈α∃programming␈α∃a␈α⊗trivial␈α∃airline␈α∃reservation␈α∃system.␈α⊗ We␈α∃want␈α∃to␈α∃say␈α⊗that␈α∃␈↓↓a
␈↓ α∧␈↓↓passenger␈α∞has␈α
a␈α∞reservation␈α
if␈α∞he␈α
has␈α∞made␈α∞one␈α
that␈α∞has␈α
not␈α∞been␈α
cancelled␈↓.␈α∞ We␈α
do␈α∞not␈α∞want␈α
to
␈↓ α∧␈↓prescribe␈α∂what␈α⊂data␈α∂structures␈α∂have␈α⊂to␈α∂be␈α∂kept␈α⊂in␈α∂order␈α∂to␈α⊂be␈α∂able␈α∂to␈α⊂answer␈α∂the␈α⊂question␈α∂of
␈↓ α∧␈↓whether someone has a reservation.

␈↓ α∧␈↓␈↓ αTThis␈α∀program␈α∀replies␈α∀properly␈α∀to␈α∀requests␈α∀to␈α∀make␈α∀reservations,␈α∀cancel␈α∀them,␈α∀and␈α∪to
␈↓ α∧␈↓inquiries␈α⊂about␈α∂whether␈α⊂a␈α⊂reservation␈α∂exists.␈α⊂ The␈α∂program␈α⊂refers␈α⊂to␈α∂its␈α⊂input␈α∂in␈α⊂terms␈α⊂of␈α∂an
␈↓ α∧␈↓abstract␈α∀analytic␈α∀syntax␈α∀the␈α∀meaning␈α∀of␈α∀whose␈α∀mnemonic␈α∀predicate␈α∀and␈α∀function␈α∀names␈α∀is
␈↓ α∧␈↓hopefully␈αobvious.␈α The␈αonly␈αdata␈αstructure␈αexplicitly␈αmentioned␈αis␈αthe␈αnumber␈αof␈α
seats␈αcurrently
␈↓ α∧␈↓occupied,␈α
and␈α
even␈α
that␈α
could␈α
be␈αeliminated␈α
from␈α
the␈α
program.␈α
 The␈α
Elephant␈αcompiler,␈α
therefore,
␈↓ α∧␈↓gets␈αthe␈α
honor␈αof␈α
determining␈αwhat␈α
other␈αdata␈α
structures␈αare␈α
needed.␈α We␈α
use␈αthe␈α
convention␈αof
␈↓ α∧␈↓writing ␈↓↓{x}f␈↓ instead of ␈↓↓f(x)␈↓ when it is convenient to write the argument before the function name.

␈↓ α∧␈↓↓␈↓ αT∀t.[output(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You had it"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE IF number(t) = N THEN "No room"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You have it now"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "It's cancelled"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have it to cancel"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF isinquiry in THEN␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You have one"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have one"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓␈↓ αT∀t.[number(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) ∨ number(t) = N
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$THEN number(t)
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t) + 1]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN number(t) - 1
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t)]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE number(t)]

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[hasrev(passenger,t)␈α∂≡␈α∂∃t1.(t1␈α∂<␈α∂t␈α∂∧␈α∂ismake␈α∞input␈α∂t1␈α∂∧␈α∂passenger␈α∂=␈α∂maker␈α∂input␈α∂t1␈α∞∧
␈↓ α∧␈↓↓number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧ iscancel input t2 ∧ maker input t2 = passenger))]␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α⊃main␈α∩difficulty␈α⊃in␈α⊃making␈α∩a␈α⊃compiler␈α∩for␈α⊃Elephant␈α⊃is␈α∩illustrated␈α⊃by␈α∩the␈α⊃predicate
␈↓ α∧␈↓␈↓↓hasrev.␈↓␈α∞The␈α∂compiler␈α∞has␈α∞to␈α∂understand␈α∞that␈α∂it␈α∞must␈α∞remember␈α∂successful␈α∞reservations␈α∂but␈α∞can
␈↓ α∧␈↓forget␈αunsuccessful␈αattempts␈αat␈αmaking␈αa␈αreservation␈αand␈αthat␈αit␈αcan␈αforget␈αreservations␈αthat␈αhave
␈↓ α∧␈↓been␈α
cancelled.␈α Perhaps␈α
␈↓↓hasrev␈↓␈αshould␈α
be␈αwritten␈α
using␈α
primitives␈αthat␈α
refer␈αexplicitly␈α
to␈αthe␈α
most
␈↓ α∧␈↓recent occurrence of an event, which might permit a less intelligent compiler.

␈↓ α∧␈↓6. Parallel processes for computing a sum of functions
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u7


␈↓ α∧␈↓␈↓ αTThe␈α∃following␈α∃Elephant␈α⊗program␈α∃computes␈α∃␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓␈α⊗using␈α∃␈↓↓k␈↓␈α∃processors.␈α⊗ A␈α∃master
␈↓ α∧␈↓processor␈α⊃with␈α⊃program␈α⊂counter␈α⊃␈↓↓pc(t)␈↓␈α⊃initializes␈α⊂the␈α⊃variables␈α⊃␈↓↓n␈↓␈α⊂and␈α⊃␈↓↓s␈↓␈α⊃and␈α⊂starts␈α⊃the␈α⊃␈↓↓k␈↓␈α⊂slave
␈↓ α∧␈↓processes␈α
whose␈α
program␈α
counters␈α
are␈α
written␈α
␈↓↓pc(i,t)␈↓␈αat␈α
step␈α
1.␈α
 A␈α
process␈α
needs␈α
exclusive␈αaccess␈α
to
␈↓ α∧␈↓␈↓↓n␈↓␈αwhen␈αit␈αis␈αreading␈αit␈αand␈αincrementing␈αit,␈αand␈αit␈αneeds␈αexclusive␈αaccess␈αto␈α␈↓↓s␈↓␈αwhen␈αincrementing
␈↓ α∧␈↓it,␈αand␈αwe␈αonly␈αprovide␈αfor␈αexclusive␈αaccess␈αat␈αthese␈αtimes.␈α We␈αimagine␈αthat␈αcomputing␈α␈↓↓f(n)␈↓␈αtakes
␈↓ α∧␈↓␈↓↓time(n)␈↓␈αunits␈αof␈α
time,␈αand␈αthese␈αoperations␈α
are␈αdone␈αin␈αparallel.␈α
 ␈↓↓pc(t)␈↓␈αis␈αthe␈αprogram␈α
counter␈αfor
␈↓ α∧␈↓the␈αmaster␈αprocess,␈αand␈α␈↓↓pc(i,t)␈↓␈αis␈αthe␈αprogram␈αcounter␈αof␈αthe␈α␈↓↓i␈↓th␈αslave␈αprocess.␈α The␈α
updating␈αof
␈↓ α∧␈↓all␈α⊃variables␈α⊃except␈α⊂the␈α⊃␈↓↓pc(i,t)␈↓␈α⊃works␈α⊃as␈α⊂in␈α⊃Algolic␈α⊃programs,␈α⊃but␈α⊂the␈α⊃latter␈α⊃requires␈α⊃a␈α⊂more
␈↓ α∧␈↓elaborate␈αand␈αsomewhat␈αimplicit␈αdescription␈αthat␈αmay␈αwell␈αchallenge␈αthe␈αdesigner␈αof␈αan␈αElephant
␈↓ α∧␈↓compiler.

␈↓ α∧␈↓↓n(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
␈↓ α∧␈↓↓␈↓ β∀ELSE n(t)

␈↓ α∧␈↓↓s(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
␈↓ α∧␈↓↓␈↓ β∀ELSE s(t)

␈↓ α∧␈↓↓m(i,t+1)␈↓ αz= ␈↓ β∀IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
␈↓ α∧␈↓↓␈↓ β∀ELSE m(i,t)

␈↓ α∧␈↓↓pc(t+1) ␈↓ αz= ␈↓ β∀IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE pc(t) + 1


␈↓ α∧␈↓↓pc(i,0) = 0

␈↓ α∧␈↓↓pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

␈↓ α∧␈↓↓pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0

␈↓ α∧␈↓↓pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3
␈↓ α∧␈↓↓␈↓ β∀⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

␈↓ α∧␈↓↓pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

␈↓ α∧␈↓↓pc(i,t) = 5 ⊃ pc(i,t+1) = 1

␈↓ α∧␈↓␈↓ αTIt␈α∩may␈α∪be␈α∩questioned␈α∪whether␈α∩the␈α∪above␈α∩Elephant␈α∪program␈α∩should␈α∪be␈α∩regarded␈α∪as␈α∩a
␈↓ α∧␈↓"program"␈α∞that␈α∞can␈α
be␈α∞compiled␈α∞by␈α∞a␈α
suitable␈α∞compiler␈α∞or␈α
as␈α∞something␈α∞between␈α∞a␈α
specification
␈↓ α∧␈↓and␈αa␈α
program.␈α Perhaps␈α
it␈αis␈α
an␈αexample␈α
of␈αthat␈α
elusive␈αconcept␈α
called␈αan␈α
algorithm.␈α Notice␈α
that
␈↓ α∧␈↓it␈α
assumes␈αthat␈α
synchronization␈αoccurs␈α
without␈αspecifying␈α
any␈αway␈α
of␈αdoing␈α
it.␈α Just␈α
the␈α
thing␈αto
␈↓ α∧␈↓challenge␈αa␈αsmart␈αcompiler␈α
or␈αautomatic␈αprogramming␈αsystem.␈α
 On␈αthe␈αother␈αhand,␈αthe␈α
correctness
␈↓ α∧␈↓of the Elephant program is given by the statement,
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u8


␈↓ α∧␈↓␈↓↓∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = ␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓

␈↓ α∧␈↓and␈α∀this␈α∀can␈α∃presumably␈α∀be␈α∀proved␈α∀from␈α∃the␈α∀program.␈α∀ The␈α∀correspondence␈α∃between␈α∀this
␈↓ α∧␈↓Elephant␈α⊗program␈α∃and␈α⊗one␈α∃that␈α⊗is␈α∃more␈α⊗explicit␈α∃about␈α⊗synchronization␈α∃might␈α⊗be␈α∃proved
␈↓ α∧␈↓separately.

␈↓ α∧␈↓␈↓ αTThere may well be better ways of describing parallel processes in Elephant.

␈↓ α∧␈↓7. Equivalence of Elephant programs.

␈↓ α∧␈↓␈↓ αTDefinitions␈α&of␈α'the␈α&equivalence␈α'of␈α&Elephant␈α'programs,␈α&equivalence-preserving
␈↓ α∧␈↓transformations␈α∩of␈α⊃programs,␈α∩and␈α⊃techniques␈α∩for␈α⊃proving␈α∩equivalence␈α⊃can␈α∩be␈α⊃expected␈α∩to␈α⊃be
␈↓ α∧␈↓important␈α∞in␈α∞applications␈α∞of␈α
Elephant.␈α∞ For␈α∞example,␈α∞one␈α
approach␈α∞to␈α∞compiling␈α∞Elephant␈α∞is␈α
to
␈↓ α∧␈↓transform the program into an immediate program using equivalence-preserving transformations.

␈↓ α∧␈↓␈↓ αTEquivalence␈α
relations␈α
should␈α
be␈α
defined␈α
that␈α
will␈α
facilitate␈α
this␈α
process.␈α
 An␈α
obvious␈αform
␈↓ α∧␈↓of␈α
equivalence␈α
is␈α
to␈α
require␈α
that␈α
each␈α
variable␈α
in␈α
the␈α
two␈α
programs␈α
be␈α
represented␈α
by␈α
the␈α
same
␈↓ α∧␈↓function␈α∪of␈α∪time␈α∪for␈α∩all␈α∪values␈α∪of␈α∪the␈α∩parameters.␈α∪ This␈α∪is␈α∪too␈α∩strict␈α∪an␈α∪equivalence␈α∪to␈α∩be
␈↓ α∧␈↓interesting␈α∂on␈α∂two␈α∂grounds.␈α∞ First,␈α∂the␈α∂two␈α∂forms␈α∂of␈α∞the␈α∂multiplication␈α∂by␈α∂addition␈α∂program␈α∞in
␈↓ α∧␈↓section␈α∞2␈α∞would␈α∞not␈α∞be␈α∞equivalent,␈α∞because␈α∞one␈α∞of␈α∞them␈α∞goes␈α∞around␈α∞the␈α∞loop␈α∞in␈α∞one␈α∞time␈α∞step
␈↓ α∧␈↓while␈αthe␈αother␈αtakes␈αfour␈αsteps.␈α Second,␈αtransforming␈αa␈αprogram␈αto␈αan␈αimmediate␈αprogram␈αmay
␈↓ α∧␈↓involve␈α
the␈αintroduction␈α
of␈αnew␈α
variables,␈α
arrays␈αand␈α
other␈αdata␈α
structures␈αin␈α
order␈α
to␈αeliminate
␈↓ α∧␈↓the direct references to the past.

␈↓ α∧␈↓␈↓ αTWe␈α⊃cannot␈α⊃␈↓↓a␈α⊃priori␈↓␈α⊃exclude␈α⊃the␈α⊂possibility␈α⊃that␈α⊃several␈α⊃concepts␈α⊃of␈α⊃equivalence␈α⊃will␈α⊂be
␈↓ α∧␈↓useful.␈α⊂ However,␈α⊂our␈α⊂first␈α⊃attempt␈α⊂is␈α⊂based␈α⊂on␈α⊂the␈α⊃idea␈α⊂that␈α⊂correspondence␈α⊂of␈α⊃times␈α⊂doesn't
␈↓ α∧␈↓matter␈α⊃so␈α⊂long␈α⊃as␈α⊃the␈α⊂correspondence␈α⊃is␈α⊂monotonic␈α⊃and␈α⊃that␈α⊂we␈α⊃are␈α⊂interested␈α⊃only␈α⊃a␈α⊂certain
␈↓ α∧␈↓correspondence between the states of the program.

␈↓ α∧␈↓␈↓ αTLet␈α∩one␈α∩Elephant␈α∩program␈α∩␈↓↓P␈↓␈α∩have␈α∩functions␈α∩␈↓↓u␈↓#v1␈↓#(t), ... ,u␈↓#vm␈↓#(t)␈↓␈α∩and␈α∩a␈α∩second␈α∩␈↓↓P'␈↓␈α∩have
␈↓ α∧␈↓functions␈α⊂␈↓↓u␈↓#v1␈↓#'(t) ... u␈↓#vn␈↓#'(t).␈↓␈α⊂In␈α⊂order␈α⊂to␈α⊂avoid␈α⊂prolixity,␈α⊂we␈α⊂shall␈α⊂summarize␈α⊂these␈α⊂functions␈α⊂as
␈↓ α∧␈↓vectors␈α
␈↓↓␈↓αu␈↓↓(t)␈↓␈αand␈α
␈↓↓␈↓αu␈↓↓'(t)␈↓.␈α Let␈α
␈↓↓EP(␈↓αu␈↓↓,␈↓αu␈↓↓')␈↓␈αbe␈α
a␈αrelation.␈α
 Let␈αthe␈α
first␈αdepend␈α
on␈αparameters␈α
␈↓↓x␈↓#v1␈↓#, ... x␈↓#vp␈↓#␈↓
␈↓ α∧␈↓and␈α
the␈α
second␈α
have␈α
parameters␈α
␈↓↓x␈↓#v1␈↓#' ... x␈↓#vq␈↓#'␈↓,␈α
similarly␈α
summarized␈α
into␈α
vectors␈α
␈↓↓␈↓αx␈↓↓␈↓␈α
and␈α∞␈↓↓␈↓αx␈↓↓'␈↓.␈α
 (The
␈↓ α∧␈↓parameters␈α∂of␈α∂the␈α∂program␈α∂for␈α∂multiplication␈α∂by␈α∞addition␈α∂were␈α∂␈↓↓m␈↓␈α∂and␈α∂␈↓↓n).␈↓␈α∂Let␈α∂␈↓↓EP(␈↓αx␈↓↓,␈↓αx␈↓↓')␈↓␈α∂be␈α∞a
␈↓ α∧␈↓relation␈αbetween␈αthe␈αparameters.␈α Also␈αlet␈α␈↓↓I(␈↓αx␈↓↓)␈↓␈αand␈α␈↓↓I'(␈↓αx␈↓↓')␈↓␈αbe␈αpredicates␈αthat␈αsay␈αwhat␈αstates␈αof␈α
the
␈↓ α∧␈↓two programs are to be compared.  Now suppose we can prove that

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ∧ EP(␈↓αx␈↓↓,␈↓αx␈↓↓') ⊃ EV(␈↓αu␈↓↓(0),␈↓αu␈↓↓'(0)) ∧ I(␈↓αu␈↓↓(0)) ∧ I'(␈↓αu␈↓↓'(0))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t2 t1'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2 >t1 ∧ I(␈↓αu␈↓↓(t2)) ⊃ ∃t2'.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓

␈↓ α∧␈↓and going the other way

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t1' t2'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2' >t1' ∧ I'(␈↓αu␈↓↓'(t2')) ⊃ ∃t2.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓.

␈↓ α∧␈↓We␈α
should␈α
then␈α
call␈α
the␈αprograms␈α
␈↓↓P␈↓␈α
and␈α
␈↓↓P'␈↓␈α
equivalent␈α
with␈αrespect␈α
to␈α
the␈α
the␈α
conditions␈α
␈↓↓I␈↓␈αand␈α
␈↓↓I'␈↓
␈↓ α∧␈↓and␈α∞the␈α∞relations␈α∞␈↓↓EP␈↓␈α∞and␈α∞␈↓↓EV.␈↓␈α∞Note␈α
that␈α∞we␈α∞have␈α∞used␈α∞the␈α∞programs␈α∞themselves␈α∞as␈α
hypotheses
␈↓ α∧␈↓since we can regard a program as the conjunction of its constituent sentences.
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u9


␈↓ α∧␈↓␈↓ αTThe two versions of multiplication by addition are equivalent with respect to the predicates

␈↓ α∧␈↓␈↓ αT␈↓↓EP(m,n,m',n') ≡ m=m' ∧ n=n'␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨ [i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]␈↓

␈↓ α∧␈↓They␈α∞should␈α∞be␈α∞sufficient␈α∞to␈α∞prove␈α∞that␈α∞one␈α∞program␈α∞is␈α∞correct␈α∞(according␈α∞to␈α∞the␈α∞definitlons␈α
of
␈↓ α∧␈↓section␈α2)␈αif␈αand␈αonly␈αif␈αthe␈αother␈αis.␈α We␈αexpect␈αto␈αgive␈αless␈αtrivial␈αexamples␈αof␈αequivalence␈αand
␈↓ α∧␈↓maybe a proof of equivalence in the final version of this paper.

␈↓ α∧␈↓␈↓ αTInput-output␈α∂equivalence,␈α⊂i.e.␈α∂that␈α⊂two␈α∂programs␈α∂give␈α⊂the␈α∂same␈α⊂output␈α∂sequence␈α⊂for␈α∂any
␈↓ α∧␈↓sequence␈αof␈α
inputs,␈αseems␈α
to␈αbe␈α
a␈αspecial␈α
case␈αof␈α
the␈αabove,␈α
and␈αthere␈α
is␈αreason␈α
to␈αhope␈α
that␈αit␈α
will
␈↓ α∧␈↓suffice for many applications.

␈↓ α∧␈↓8. Remarks

␈↓ α∧␈↓1.␈αPrograms␈αin␈αLucid␈α(Ashcroft␈αand␈αWadge␈α1976)␈αare␈αalso␈αcollections␈αof␈αsentences␈αin␈αa␈αfirst␈αorder
␈↓ α∧␈↓language.␈α A␈αLucid␈αobject␈αis␈αa␈αvector␈α
of␈αthe␈αvalues␈αof␈αa␈αvariable␈αthroughout␈αtime.␈α
 This␈αpermits
␈↓ α∧␈↓some␈α
statements␈α∞to␈α
be␈α∞made␈α
in␈α∞a␈α
very␈α∞neat␈α
way.␈α
 However,␈α∞it␈α
seems␈α∞to␈α
be␈α∞less␈α
flexible␈α∞than␈α
the
␈↓ α∧␈↓Elephant␈α∞device␈α∞of␈α∞admitting␈α∞the␈α∞time␈α∞as␈α∞an␈α∞explicit␈α∞parameter.␈α∞ Lucid␈α∞programs␈α∞do␈α∞not␈α∞admit
␈↓ α∧␈↓␈↓αgo to␈↓s,␈αand␈α
there␈αare␈α
other␈αunexpected␈α
restrictions.␈α Perhaps␈α
some␈αof␈α
Lucid's␈αproblems␈α
would␈αbe
␈↓ α∧␈↓cured by including the history of the program counter as a variable.

␈↓ α∧␈↓2.␈αThe␈αproperties␈αof␈αElephant␈αprograms␈αdon't␈αdepend␈αon␈αtime␈αtaking␈αinteger␈αvalues.␈α All␈αwe␈αneed
␈↓ α∧␈↓require␈αis␈αthat␈αthe␈αset␈αof␈αtimes␈αbe␈αordered␈αand␈αunbounded␈αabove.␈α Then␈αthe␈αfirst␈αsentence␈αof␈αthe
␈↓ α∧␈↓product program would take the form

␈↓ α∧␈↓␈↓↓∀t ∃t'.[t' > t ∧ i(t') ␈↓ ∧~= ␈↓ ∧4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧4ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ ∧4ELSE i(t)].

␈↓ α∧␈↓3.␈α∂It␈α∞seems␈α∂to␈α∂me␈α∞that␈α∂any␈α∂language␈α∞that␈α∂purports␈α∞to␈α∂allow␈α∂the␈α∞user␈α∂to␈α∂say␈α∞what␈α∂he␈α∂wants␈α∞the
␈↓ α∧␈↓computer␈αto␈α
do␈αin␈α
English,␈αshould␈α
allow␈αthe␈α
executive␈αor␈αgeneral␈α
or␈αother␈α
big␈αshot␈α
to␈αsay␈α
that␈α␈↓↓a
␈↓ α∧␈↓↓customer␈αhas␈αa␈αreservation␈αif␈αhe␈αhas␈αmade␈αone␈αand␈αit␈αhasn't␈αbeen␈αcancelled␈↓.␈α The␈αbig␈αshot␈αcertainly
␈↓ α∧␈↓doesn't␈α⊂want␈α⊂to␈α∂concern␈α⊂himself␈α⊂with␈α⊂what␈α∂data␈α⊂structures␈α⊂are␈α⊂required␈α∂in␈α⊂order␈α⊂to␈α⊂fulfill␈α∂his
␈↓ α∧␈↓wishes,␈α∩and␈α∪Elephant␈α∩shows␈α∩that␈α∪his␈α∩wishes␈α∩can␈α∪be␈α∩stated␈α∩without␈α∪mentioning␈α∩such␈α∪a␈α∩data
␈↓ α∧␈↓structure.

␈↓ α∧␈↓4.␈α∂In␈α∂its␈α∂present␈α∂state,␈α∂Elephant␈α∞doesn't␈α∂seem␈α∂to␈α∂be␈α∂a␈α∂very␈α∞easy␈α∂language␈α∂to␈α∂use.␈α∂ I␈α∂say␈α∞"seem",
␈↓ α∧␈↓because␈αthe␈αawkward␈αprograms␈αmay␈αbe␈αmerely␈αa␈αconsequence␈αof␈αinexperience.␈α Of␈αcourse,␈αAlgolic
␈↓ α∧␈↓programs are easy enough to write in Elephant.

␈↓ α∧␈↓5.␈α∞Regarded␈α
simply␈α∞as␈α∞a␈α
way␈α∞of␈α
writing␈α∞Algolic␈α∞programs␈α
as␈α∞logical␈α
sentences,␈α∞Elephant␈α∞plays␈α
a
␈↓ α∧␈↓role␈α⊃similar␈α⊂to␈α⊃that␈α⊃played␈α⊂by␈α⊃the␈α⊃Cartwright␈α⊂way␈α⊃of␈α⊃writing␈α⊂Lisp␈α⊃style␈α⊃recursive␈α⊂conditional
␈↓ α∧␈↓expression␈α∂programs␈α∂as␈α⊂logical␈α∂sentences.␈α∂ In␈α⊂fact␈α∂it␈α∂may␈α⊂be␈α∂a␈α∂kind␈α⊂of␈α∂dual␈α∂to␈α⊂the␈α∂Cartwright
␈↓ α∧␈↓method␈α∂just␈α∂as␈α∂␈↓↓inductive␈α∞assertions␈↓␈α∂and␈α∂␈↓↓subgoal␈α∂induction␈↓␈α∞seem␈α∂to␈α∂be␈α∂duals.␈α∂ Namely,␈α∞Elephant
␈↓ α∧␈↓programs␈αand␈αinductive␈αassertions␈αwork␈αfrom␈αan␈αinitial␈αstate␈αand␈αdescribe␈αits␈αchanges,␈αwhile␈αLisp
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f10


␈↓ α∧␈↓style␈α∂programs␈α∂and␈α∂subgoal␈α∂induction␈α∂work␈α∂backwards␈α∂from␈α∂desired␈α∂final␈α∂result.␈α∂ Thus␈α∂it␈α∂may
␈↓ α∧␈↓complete a pattern of methods of program formalization.

␈↓ α∧␈↓6.␈α∞Elephant␈α∞may␈α∞be␈α∞expanded␈α∞by␈α∞relaxing␈α∞the␈α∞restriction␈α∞that␈α∞statements␈α∞refer␈α∞only␈α∞to␈α∞the␈α
past.
␈↓ α∧␈↓Our␈α⊂big␈α⊂shot␈α∂may␈α⊂wish␈α⊂to␈α∂say,␈α⊂␈↓↓"When␈α⊂the␈α⊂passengers␈α∂arrive␈α⊂at␈α⊂the␈α∂airport␈α⊂for␈α⊂the␈α⊂flight,␈α∂an
␈↓ α∧␈↓↓airplane␈α⊃and␈α⊂a␈α⊃crew␈α⊃will␈α⊂have␈α⊃been␈α⊃summoned␈α⊂by␈α⊃the␈α⊂scheduling␈α⊃program␈α⊃to␈α⊂fly␈α⊃them␈α⊃to␈α⊂their
␈↓ α∧␈↓↓destination"␈↓.␈α∞ Allowing␈α
the␈α∞right␈α
hand␈α∞sides␈α
of␈α∞Elephant␈α
equations␈α∞to␈α
refer␈α∞to␈α
the␈α∞future␈α∞puts␈α
a
␈↓ α∧␈↓heavier␈αburden␈αon␈αthe␈αcompiler.␈α In␈αfact,␈αa␈αfuturistic␈αElephant␈αprogram␈αmay␈αbe␈αcontradictory␈α
and
␈↓ α∧␈↓hence␈α
uncompilable.␈α Thus␈α
a␈αcompiler␈α
for␈α
futuristic␈αElephant␈α
is␈αreally␈α
a␈αkind␈α
of␈α
problem␈αsolver.
␈↓ α∧␈↓Only␈α⊃the␈α⊃future␈α⊃can␈α⊃tell␈α⊂if␈α⊃this␈α⊃style␈α⊃of␈α⊃programming␈α⊂will␈α⊃prove␈α⊃useful␈α⊃or␈α⊃even␈α⊂theoretically
␈↓ α∧␈↓illuminating.

␈↓ α∧␈↓7.␈αThe␈αtwo␈αaspects␈αof␈α
Elephant,␈αexplicit␈αuse␈αof␈αthe␈αtime␈α
and␈αprogram␈αcounter␈αand␈αreference␈αto␈α
the
␈↓ α∧␈↓past,␈α∂may␈α∂be␈α∂separated.␈α∂ The␈α∂first␈α∂all␈α∞by␈α∂itself␈α∂provides␈α∂the␈α∂proper␈α∂formalization␈α∂of␈α∞sequential
␈↓ α∧␈↓programs,␈α
and␈α∞there␈α
are␈α∞probably␈α
other␈α∞ways␈α
of␈α
referring␈α∞to␈α
the␈α∞past␈α
than␈α∞by␈α
using␈α∞an␈α
explicit
␈↓ α∧␈↓time␈α⊃variable,␈α⊃e.g.␈α⊃modal␈α⊃tense␈α⊃operators␈α⊃might␈α∩be␈α⊃used.␈α⊃ One␈α⊃of␈α⊃these␈α⊃ways␈α⊃might␈α∩be␈α⊃more
␈↓ α∧␈↓convenient.

␈↓ α∧␈↓9. References

␈↓ α∧␈↓␈↓αAshcroft,␈α∞E.␈α∞A.␈α∞and␈α∞W.␈α∞W.␈α∞Wadge␈α∞(1976)␈↓:␈α∞Lucid␈α∞-␈α∞A␈α∞Formal␈α∞System␈α∞for␈α∞Writing␈α∞and␈α∞Proving
␈↓ α∧␈↓Programs, ␈↓↓Siam Journal of Computing␈↓, Vol. 5, No. 3, September.

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1976)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed
␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.

␈↓ α∧␈↓␈↓αCartwright,␈α⊃Robert␈α⊂and␈α⊃John␈α⊂McCarthy␈α⊃(1979)␈↓:␈α⊃"Recursive␈α⊂Programs␈α⊃as␈α⊂Functions␈α⊃in␈α⊃a␈α⊂First
␈↓ α∧␈↓Order␈α
Theory",␈α
in␈α
E.␈α
Blum␈α
and␈α
S.␈αTakasu␈α
(eds.),␈α
␈↓↓Proceedings␈α
of␈α
the␈α
International␈α
Conference␈αon
␈↓ α∧␈↓↓Mathematical Studies of Information Processing␈↓, Springer Publishers.

␈↓ α∧␈↓␈↓αMcCarthy, John and Carolyn Talcott (1979)␈↓: ␈↓↓LISP: Programming and Proving␈↓, (in preparation)


␈↓ α∧␈↓This partial draft of ELEPHA[S79,JMC] compiled at 16:29 on June 5, 1979.